import atom.UnaryAtom;
import formula.*;
import literal.UnaryLiteral;
import proof.ConclusionProof;
import proof.Proof;
import proof.ProofRule;
import proof.DerivedProof;
import sign.FormulaSign;

import java.util.ArrayList;

public class testRule {
    public static void main(String[] args) {
        //D1Test();
//        test B rule
//        Btest();
//        测试D2
       D2test();
//        D3 test
//        D3test();

        //B_D1Test();
       //D1_D2Test();
        //XTest();
        //ITest();
        //TTest();
        //ATest();
        //ANY_ANYTest();
        //EETest();
        //AETest();
    }

    public static void Btest(){//验证rule B
        // {ANY(p,q),ANY(q,l)}B -> ANY(p,l)
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        Formula l=new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"),false));
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,p,q);
        BinaryFormula f2=new BinaryFormula(FormulaSign.ANY,q,l);

        Proof p1 = new ConclusionProof(f1);
        Proof p2 = new ConclusionProof(f2);

        ArrayList<Proof> ps=new ArrayList<>();
        ps.add(p1);
        ps.add(p2);

        Proof proof=new DerivedProof(ps, ProofRule.B);
        System.out.println(proof.toString());
    }

    public static void D1Test(){//{ANY(q,l),Exist(p,q)}D1 -> Exist(p,l)
        UnaryFormula a=new UnaryFormula(new UnaryLiteral(new UnaryAtom("a"),false));
        Formula b=new UnaryFormula(new UnaryLiteral(new UnaryAtom("b"),false));
        Formula c=new UnaryFormula(new UnaryLiteral(new UnaryAtom("c"),false));
        Formula d=new UnaryFormula(new UnaryLiteral(new UnaryAtom("d"),false));
        BinaryFormula f1=new BinaryFormula(FormulaSign.EXIST,a,b);
        BinaryFormula f2=new BinaryFormula(FormulaSign.ANY,c,d);
        BinaryFormula conclusion=new BinaryFormula(FormulaSign.EXIST,a,d);
        Proof out =new ConclusionProof(conclusion);

        ArrayList<Proof> proofs=new ArrayList<>();
        proofs.add(new ConclusionProof(f2));
        proofs.add(new ConclusionProof(f1));
        System.out.println(new DerivedProof(proofs,ProofRule.D1));
    }

    public static void D2test(){//[{Exist(p,l),ANY(p,q)}D2 -> Exist(q,l)]
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        Formula l=new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"),false));
        BinaryFormula f4=new BinaryFormula(FormulaSign.EXIST,p,l);
        BinaryFormula f5=new BinaryFormula(FormulaSign.ANY,p,q);
        ArrayList<Proof> D2=new ArrayList<>();
        Proof p4=new ConclusionProof(f4);
        Proof p5=new ConclusionProof(f5);
        D2.add(p4);
        D2.add(p5);
        Proof proof=new DerivedProof(D2, ProofRule.D2);
        //System.out.println(proof);
        //测试solveHelper
        BinaryFormula conclusion=new BinaryFormula(FormulaSign.EXIST,q,l);
        ArrayList<Formula> arrayList=new ArrayList<>();
        arrayList.add(f4);
        arrayList.add(f5);
        System.out.println(Solve.solve(arrayList,conclusion));
    }

    public static void D3test(){//[{ANY(q,not l),Exist(p,l)}D3 -> Exist(p,not q)]
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        Formula l=new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"),false));
        Formula not_l=new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"),true));
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,q,not_l);
        BinaryFormula f2=new BinaryFormula(FormulaSign.EXIST,p,l);
        ArrayList<Proof> D3=new ArrayList<>();
        Proof p1=new ConclusionProof(f1);
        Proof p2=new ConclusionProof(f2);
        D3.add(p1);
        D3.add(p2);
        Proof proof=new DerivedProof(D3, ProofRule.D3);
        System.out.println(proof);

    }

    public static void B_D1Test(){ //rule B +rule D1
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        Formula m=new UnaryFormula(new UnaryLiteral(new UnaryAtom("m"),false));
        Formula l=new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"),false));
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,p,q);
        BinaryFormula f2=new BinaryFormula(FormulaSign.ANY,q,l);
        BinaryFormula f3=new BinaryFormula(FormulaSign.EXIST,m,p);


        Formula conclusion=new BinaryFormula(FormulaSign.EXIST,m,l);//最终结论
        ArrayList<Formula> formulas=new ArrayList<>();
        formulas.add(f1);
        formulas.add(f2);
        formulas.add(f3);
        System.out.println(Solve.solve(formulas,conclusion));
    }

    public static void D1_D2Test(){ //rule D1 +rule D2
        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
        Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        Formula l=new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"),false));
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,q,l);
        BinaryFormula f2=new BinaryFormula(FormulaSign.EXIST,p,q);
        BinaryFormula f3=new BinaryFormula(FormulaSign.ANY,p,q);

        Formula conclusion=new BinaryFormula(FormulaSign.EXIST,q,l);//最终结论
        ArrayList<Formula> formulas=new ArrayList<>();
        formulas.add(f1);
        formulas.add(f2);
        formulas.add(f3);
        System.out.println(Solve.solve(formulas,conclusion));
    }

//    public static void XTest(){ //rule X: Exist(p,q),ANY(p,not q)->terminal
//        UnaryFormula p=new UnaryFormula(new UnaryLiteral(new UnaryAtom("p"),false));
//        Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
//        Formula not_q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),true));
//        Formula l=new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"),false));
//
//        BinaryFormula f1=new BinaryFormula(FormulaSign.EXIST,p,q);
//        BinaryFormula f2=new BinaryFormula(FormulaSign.ANY,p,not_q);
//
//        Formula conclusion=new BinaryFormula(FormulaSign.EXIST,q,l);//最终结论，这个随便写，因为不会被访问到
//        ArrayList<Formula> formulas=new ArrayList<>();
//        formulas.add(f1);
//        formulas.add(f2);
//
////        for (Formula f:formulas) {
////            System.out.println(f.toString());
////        }
//
//        ArrayList<Proof> conditions=new ArrayList<>();
//        for (Formula f:formulas) {
//            conditions.add(new ConclusionProof(f));
//        }
//
////        Proof proof=Solve.solveHelper(conditions,conclusion,new UsedCondition());
////        if (proof.getConclusion().equals(null)){
////
////        }
////        System.out.println();
//
//
//        Proof proof=new RuleProof(conditions, ProofRule.X);
//        System.out.println(proof);//输出有点问题，要修改。
//    }

    public static void ITest(){ //rule I
        UnaryFormula d=new UnaryFormula(new UnaryLiteral(new UnaryAtom("d"),false));
        Formula l=new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"),false));

        BinaryFormula f1=new BinaryFormula(FormulaSign.EXIST,d,l);

        Formula conclusion=new BinaryFormula(FormulaSign.EXIST,d,d);//最终结论

        ArrayList<Formula> formulas=new ArrayList<>();
        formulas.add(f1);

        ArrayList<Proof> conditions=new ArrayList<>();
        for (Formula f:formulas) {
            conditions.add(new ConclusionProof(f));
        }
        Proof proof=new DerivedProof(conditions, ProofRule.I);
        System.out.println(proof);

       // System.out.println(Solve.solve(formulas,conclusion));
    }

//    public static void TTest(){ //rule T
//        UnaryFormula d=new UnaryFormula(new UnaryLiteral(new UnaryAtom("d"),false));
//        Formula l=new UnaryFormula(new UnaryLiteral(new UnaryAtom("l"),false));
//
//        BinaryFormula f1=new BinaryFormula(FormulaSign.EXIST,d,l);
//
//
//        ArrayList<Formula> formulas=new ArrayList<>();
//        formulas.add(f1);
//
//        ArrayList<Proof> conditions=new ArrayList<>();
//        for (Formula f:formulas) {
//            conditions.add(new ConclusionProof(f));
//        }
//        Proof proof=new RuleProof(conditions, ProofRule.T);
//        System.out.println(proof);
//    }

    public static void ATest(){ //rule A

        Formula q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),false));
        Formula not_q=new UnaryFormula(new UnaryLiteral(new UnaryAtom("q"),true));
        BinaryFormula f1=new BinaryFormula(FormulaSign.ANY,q,not_q);

        ArrayList<Formula> formulas=new ArrayList<>();
        formulas.add(f1);

        ArrayList<Proof> conditions=new ArrayList<>();
        for (Formula f:formulas) {
            conditions.add(new ConclusionProof(f));
        }

        Proof proof=new DerivedProof(conditions, ProofRule.A);
        System.out.println(proof);
    }





}
